\begin{tabbing}
$\forall$${\it es}$:ES, $A$, $V$:Type, $i$:Id, ${\it knd}$:Knd, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $f$:(State(${\it ds}$)$\rightarrow$$V$$\rightarrow$($A$ + Top)).
\\[0ex]($\forall$$e$:E.
\\[0ex](loc($e$) = $i$) $\Rightarrow$ (kind($e$) = ${\it knd}$) $\Rightarrow$ ((valtype($e$) $\subseteq$r $V$) \& (state@loc($e$) $\subseteq$r State(${\it ds}$))))
\\[0ex]$\Rightarrow$ \=($\forall$$e$:E.\+
\\[0ex]($\uparrow$($e$ $\in_{b}$ es{-}trigger(${\it es}$;$i$;${\it knd}$;${\it ds}$;$f$)))
\\[0ex]$\Rightarrow$ (es{-}trigger(${\it es}$;$i$;${\it knd}$;${\it ds}$;$f$)($e$) = outl($f$((state when $e$),val($e$))) $\in$ $A$))
\-
\end{tabbing}